Nuprl Lemma : not_assert_elim
9,38
postcript
pdf
b
:
. (
(
b
))
(
b
= ff)
latex
ProofTree
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
Unit
,
,
False
,
A
,
,
tt
,
,
ff
Lemmas
bool
wf
,
assert
wf
,
not
wf
,
assert
of
tt
,
bfalse
wf
origin
b:
. (
(
b)) 
(b = ff)
b:. ((b)) (b = ff)
T Qx:A. B(x)A
